﻿using System;
using System.Collections.Generic;
using System.ComponentModel;
using System.Data;
using System.Drawing;

using System.Text;
using System.Windows.Forms;
using MathAssistLibrary;
using System.Diagnostics;

namespace 命题证明
{
    public partial class frmProve : Form, IForm
    {
        public frmProve()
        {
            InitializeComponent();
        }
        TextBox textBox;
 

        private void txtKnown_Enter( object sender, EventArgs e )
        {
            textBox = txtKnown;
        }

        private void txtResult_Enter( object sender, EventArgs e )
        {
            textBox = txtResult;
        }
        frmProve frm;
        Form IForm.GetForm
        {
            get
            {
                if ( frm == null || frm.IsDisposed )
                    frm = new frmProve();
                return frm;
            }
        }
        string IForm.Text
        {
            get { return "逻辑命题证明"; }
        }


        private void toolStripButton_Click( object sender, EventArgs e )
        {
            ToolStripButton btn = sender as ToolStripButton;
            char c = Convert.ToChar( Convert.ToInt32( btn.Tag ) );
            string text = textBox.Text;
            int start = textBox.SelectionStart;
            text = text.Insert( textBox.SelectionStart, c.ToString() );

            textBox.Text = text;
            textBox.SelectionStart = start + 1;
        }

        private void tsButtonProve_Click( object sender, EventArgs e )
        {
            Prove();
        }

        private void Prove()
        {
            ResultProve prove = new ResultProve();
            txtKnown.Text = txtKnown.Text.Replace( " ", "" );
            txtResult.Text = txtResult.Text.Replace( " ", "" );
            gridViewResult.Rows.Clear();
            toolLabelMessage.Text = "";
            List<string> conditions = new List<string>( txtKnown.Text.Split( new char[] { ',' } ) );
            try
            {
                Stopwatch sw = Stopwatch.StartNew();
                List<ResultParameter> process = prove.Prove( conditions, txtResult.Text );
                sw.Stop();
                if ( process != null )
                {
                    for ( int i = 0; i < process.Count; ++i )
                    {
                        List<object> rows = new List<object>();
                        string previous = "";
                        for ( int j = 0; j < process[i].Previous.Count; ++j )
                        {
                            previous += process[i].Previous[j].ToString() + " ";
                        }
                        previous += process[i].LawName;
                        rows.Add( previous );
                        rows.Add( process[i].Content );
                        rows.Add( i.ToString() );
                        gridViewResult.Rows.Add( rows.ToArray() );
                    }
                    toolLabelMessage.Text = string.Format( "证明过程用时:{0}秒", sw.Elapsed.TotalSeconds.ToString( "F3" ) );
                }
                else
                {
                    toolLabelMessage.Text = "这个结论还不能被证明，可能是因为条件不全或本程序还不完善";
                }
                lstConditions.Items.Clear();
                foreach ( ProveNode n in prove.conditions )
                {
                    lstConditions.Items.Add( n.Result + "\t" + n.ProveName );
                }
            }
            catch ( ExpressionException value )
            {
                toolLabelMessage.Text = string.Format( "{0}。出错位置{1}", value.Message, value.Index );
            }
        }

        private void tsmiExample_Click( object sender, EventArgs e )
        {
            frmExample f = new frmExample();
            f.Show();
        }

        private void txtKnown_KeyDown( object sender, KeyEventArgs e )
        {
            if ( e.KeyData == Keys.Enter )
            {
                txtResult.Focus();
            }
        }

        private void txtResult_KeyDown( object sender, KeyEventArgs e )
        {
            if ( e.KeyData == Keys.Enter )
                Prove();
        }

        private void frmProve_Load( object sender, EventArgs e )
        {
            textBox = txtKnown;
        }

        private void tsmiBig_Click( object sender, EventArgs e )
        { 
            Font = new Font("宋体" ,15);
        }

        private void tsmiExit_Click( object sender, EventArgs e )
        {
            Application.Exit();
        }

    }
}
